| Definitions |  x:A. B(x), P   Q, f || g, A ||+ B, (with ds: ds action a:T precondition a(v) is P s v), with ds: ds init: initaction a:T precondition a(v) is P, P & Q, M1 || M2, ma-frame-compatible(A;B), mk-ma, x : v, , M1 ||decl M2, 1of(t), 2of(t), Prop,  b, x  dom(f), f(x), deq-member(eq;x;L), reduce(f;k;as), false , Y, if b t else f fi, t T, P  Q, P Q, ma-frame-compat(A;B), xdom(f). v=f(x) P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), z != f(x) P(a;z),  x. t(x), a:A fp B(a),  A, False, P  Q, x(s) |
